from z3 import *

Z = IntSort()
Tree = Datatype("Tree")
Tree.declare("Empty")
Tree.declare("Node", ("left", Tree), ("data", Z), ("right", Tree))
Tree = Tree.create()
t = Const("t", Tree)
solve(t != Tree.Empty)
# > [t = Node(Empty, 0, Empty)]

prove(t != Tree.Node(t, 0, t))
# > proved
